(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)


(** ** MIO: Generation of Zero Matrix and Unit Matrix *)
Require Import List.
Require Import Matrix.Mat.Mat_def.
Require Import Matrix.Mat.list_function.


Section Matrix_io.

Variable A:Set.
Variable Zero:A.
Variable One:A.

(* ################################################################# *)
(** * Generation of Zero Matrix *)

Section Matrix_o.

(** ** Functions of Zero List and Two-dimensional list *)

Section Zero_list_dlist.

(** *** list_o *)
(** [Zero;Zero;...;Zero],of which the length is n. *)
Fixpoint list_o n :=
  match n with
  | O => List.nil
  | S n' => List.cons Zero (list_o n')
  end.

(** *** dlist_o *)
(** [[Zero;Zero;...;Zero];...[Zero;Zero;...;Zero]], of which the 
    height is m and the width is n. *)
Fixpoint dlist_o m n:=
  match m with
  | O => List.nil
  | S m' => List.cons (list_o n) (dlist_o m' n)
  end.

End Zero_list_dlist.

(** ** Properties of Functions of Zero List and Two-dimensional List *)

Section Zero_list_dlist_lemma.

(** *** list_o_length *)
(* The length of the list generated by list_o n is n. *)
Lemma list_o_length : forall n , 
  length (list_o n) = n.
Proof.
  intros.
  induction n.
  - simpl. auto.
  - simpl. f_equal. auto.
Qed.

(** *** dlist_o_length *)
(** The height of the two-dimensional list generated by dlist_o is m. *)
Lemma dlist_o_height : forall m n ,
   length (dlist_o m n) = m.
Proof.
  intros.
  induction m.
  simpl.
  auto.
  simpl. f_equal. auto.
Qed.

(** *** dlist_o_width *)
(** The width of the two-dimensional list generated by dlist_o is n. *)
Lemma dlist_o_width : forall m n ,
   width (dlist_o m n) n.
Proof.
  intros.
  induction m.
  induction n.
  - simpl. auto.
  - simpl. auto.
  - induction n.
    + simpl. auto.
    + simpl. split. f_equal. apply list_o_length. auto.
Qed.

End Zero_list_dlist_lemma.

(** ** MO *)
(** Generate a zero matrix with height m and width n. *)
Definition MO m n :=
  let dl := dlist_o m n in
  mkMat A m n dl (dlist_o_height m n) (dlist_o_width m n).

(** *** dlist_o_m_0 *)
Lemma dlist_o_m_0: forall m,
  dlist_o m 0 = nil_list A m.
Proof.
  induction m.
  - auto. - simpl. f_equal. apply IHm.
Qed.

Lemma list_o_app: forall n1 n2,
  list_o n1 ++ list_o n2 = list_o (n1+n2).
Proof.
  induction n1. simpl. auto.
  induction n2. simpl. f_equal. rewrite app_nil_r.
  auto. simpl. f_equal. rewrite <-IHn1.
  f_equal.
Qed.

Lemma dlist_o_app: forall m1 m2 n2,
  dlist_o (m1+m2) n2 
  = (dlist_o  m1 n2) ++(dlist_o  m2 n2).
Proof.
  induction m1. simpl. auto.
  induction m2. simpl. intros. f_equal. rewrite app_nil_r.
  auto. induction n2. simpl. f_equal. rewrite ?dlist_o_m_0.
  rewrite nil_list_app. f_equal. simpl.
  f_equal. rewrite IHm1. f_equal.
Qed.

End Matrix_o.

(** * Generation of Unit Matrix *)

Section Matrix_I.

(** ** Functions of Unit List and Two-dimensional List *)

Section One_list_dlist.

(** *** list_i *)
(** Generate a list with the i-th element as One, the rest elements
    as Zero, and a length of n. *)
Fixpoint list_i n i :=
  match n,i with
  | O,_ =>List.nil
  | S n',O => List.cons Zero (list_i n' O)
  | S n',S O => List.cons One (list_i n' O)
  | S n', S i' => List.cons Zero (list_i n' i')
  end.


(** *** dlist_i' *)
(** This function helps to realize the unit matrix generating
    function. It generates a two-dimensional list of length n
    with decreasing position of One element. *)
Fixpoint dlist_i' m n i :=
  match m with
  | O => List.nil
  | S m' => List.cons (list_i n (S i)) (dlist_i' m' n (S i))
  end.

Lemma height_dlist_i' : forall m n i ,
  height (dlist_i' m n i) = m.
Proof.
  induction m.
  - simpl. auto.
  - simpl. intros. f_equal. auto.
Qed.

End One_list_dlist.

(** ** Properties of Functions of Unit List and Two-dimensional List *)

Section One_list_dlist_lemma.

(** *** width_app *)
(** This is an auxiliary lemma, the relationship between width and app. *)
Lemma width_app : forall {A:Set} (l1 l2:list (list A)) (n:nat),
   width (l1++l2) n <->
   width l1 n /\ width l2 n.
Proof.
  induction l1.
  induction l2.
  - split. + simpl. auto. + simpl. auto.
  - split. + simpl. intros. split. auto. apply H.
           + simpl. intros. inversion H. apply H1.
  - split. + intros. simpl. split. inversion H.
             split. apply H0. apply IHl1 in H1.
             destruct H1. apply H1. inversion H. 
             apply IHl1 in H1.
             destruct H1. apply H2.
           + intros. simpl. inversion H. inversion H0.
             split. apply H2. apply IHl1. split.
             apply H3. apply H1.
Qed.

(** *** list_i_length *)
(** list_i n m produces a list of length n. *)
Lemma length_list_i : forall m n ,
  length (list_i n m) = n.
Proof.
  induction m.
  induction n.
  - simpl. auto.
  - simpl. f_equal. auto.
  - induction n.
    + simpl. auto.
    + simpl. induction m. simpl. auto. simpl. auto.
Qed.

(** *** width_rev *)
(** The width of the two-dimensional list is unchanged
    after rev transformation. *)
Lemma width_rev : forall (m:list (list A)) (n:nat),
   width m n -> width (rev m) n.
Proof.
  induction m. induction n.
  - simpl. auto.
  - simpl. auto.
  - induction n.
    + simpl. intros. apply width_app. simpl. destruct H.
      rewrite H. auto.
    + simpl. intros. apply width_app. simpl.
      destruct H. rewrite H. auto.
Qed.
Lemma width_dlist_i':forall m n i, 
  width  (dlist_i' m n i) n.
Proof.
  induction m. simpl. auto.
  induction n. simpl. auto. 
  split. apply length_list_i. apply IHm.
Qed. 

Lemma list_i_n_0: forall n,
  list_i n 0 = list_o n.
Proof.
  induction n. simpl. auto.
  simpl. f_equal. auto.
Qed.

End One_list_dlist_lemma.

(** ** MI *)
(** Generate an identity matrix with height and width n. *)
Definition MI n := 
let ma := dlist_i' n n 0 in
  mkMat A n n ma (height_dlist_i' n n 0) (width_dlist_i' n n 0).

End Matrix_I.

End Matrix_io.
(*
Require Import Reals.
Open Scope R.
Import ListNotations.
Section test.

  Definition tm1:= dlist_i' R 0 1 3%nat 3%nat 0%nat.
  Definition tm2:= [[1;0;0];[0;1;0];[0;0;1]].

  Lemma eq1: tm1= tm2.
  Proof. unfold tm1,tm2. unfold dlist_i',list_i.
  simpl. auto.
  Qed.
End test.
  *)

